(* pretty printer cubicle *)


type op_comp = Eq | Lt | Le | Neq
type op_arith = Plus | Minus

type const = ConstInt of int32 | ConstReal of float | ConstName of string

type term = 
  | Const of const
  | Elem of string
  | Access of string * string list
  | Arith of term * op_arith * const
      
module rec Atom : sig
  type t =
    | True
    | False
    | Comp of term * op_comp * term                                        
    | Ite of SAtom.t * t * t

  val compare : t -> t -> int

end = struct
    
  type t =
    | True
    | False
    | Comp of term * op_comp * term
    | Ite of SAtom.t * t * t

  let rec compare = Pervasives.compare 

end
and SAtom : Set.S with type elt = Atom.t = Set.Make(Atom)

module SSAtom : Set.S with type elt = SAtom.t = Set.Make(SAtom)

open Atom

type update = {
  up_arr : string;
  up_arg : string list;
  up_swts : (SAtom.t * term) list;
}

type transition = {
  tr_name : string;
  tr_args : string list;
  tr_reqs : SAtom.t;
  tr_ureq : (string * SAtom.t list) list;
  tr_assigns : (string * term) list;
  tr_arrass : (string * string list * term) list;
  tr_upds : update list;
  tr_nondets : string list
}

type assign = Avar of string * term | Aarray of string * string list * term
    
type elem = string * (string list)

type decl = Dglobal of string * string | Dconst of string * string
            | Darray of string * (string list * string)

type decls =
  | Dlist of decl list
  | Dapp of decls * decls

let nop = Dlist []

let decl_l l = Dlist l

let (++) c1 c2 = Dapp (c1, c2)

type state =
  | Sinit of string option * SAtom.t
  | Sinv of (string list * SAtom.t)
  | Scand of string
  | Sunsafe of (string list * SAtom.t)
  | Sforward of (string list * string list * SAtom.t)
  | Strans of transition

type states =
  | Slist of state list
  | Sapp of states * states

let nost = Slist []

let state_l l = Slist l

let (+++) c1 c2 = Sapp (c1, c2)

type qdnf =
  | QDnone of SSAtom.t
  | QDexists of string * SSAtom.t
  | QDforall of string * SSAtom.t
      
type system = {
  num_procs : int;
  type_defs : elem list;
  decls : decls;
  (* unsafes : string *)
  states : states;
}
    
(* Pretty-printer *)

open Format 

let idt = "\t"

let rec print_sep_elmt sep fmt f = function
| [] -> ()
| [e] -> fprintf fmt "%a" f e
| s::t -> begin fprintf fmt "%a%s" f s sep; print_sep_elmt sep fmt f t end

let print_op_comp fmt = function
| Eq -> fprintf fmt "="
| Lt -> fprintf fmt "<"
| Le -> fprintf fmt "<="
| Neq -> fprintf fmt "<>"

let print_const fmt = function
| ConstInt n -> fprintf fmt "%s" (Int32.to_string n)
| ConstReal n -> fprintf fmt "%s" (string_of_float n)
| ConstName s -> fprintf fmt "%s" s

let rec print_term fmt = function
| Const c -> print_const fmt c
| Elem (str) -> fprintf fmt "%s" str
| Access (str, strl) -> fprintf fmt "%s[" str;
    print_sep_elmt "," fmt (fun fmt s -> fprintf fmt "%s" s) strl;
    fprintf fmt "]"
| Arith (term, Plus, cst) ->
    fprintf fmt "%a + %a" print_term term print_const cst
| Arith (term, Minus, cst) ->
    fprintf fmt "%a + %a"
      print_term term print_const cst  (* Attention, signe +/- *)

let rec print_atom fmt = function
| True -> fprintf fmt "True"
| False -> fprintf fmt "False"
| Comp (t1, op, t2) -> fprintf fmt "%a %a %a"
    print_term t1 print_op_comp op print_term t2
| Ite (sa, a1, a2) -> fprintf fmt "ite %a %a %a"
    (print_satom true) sa print_atom a1 print_atom a2
(* Je ne vois pas à quoi ça correspond *)

and print_satom indent fmt sa =
  if indent then fprintf fmt "%s" idt;
  print_sep_elmt " && " fmt print_atom (SAtom.elements sa) 
    
let print_update fmt u =
  fprintf fmt "%s[" u.up_arr;
  print_sep_elmt "," fmt (fun fmt s -> fprintf fmt "%s" s) u.up_arg;
  fprintf fmt "] := case\n";
  print_sep_elmt "\n" fmt (fun fmt (atoms, term) ->
    fprintf fmt "| %a : %a" (print_satom true) atoms print_term term 
  ) u.up_swts;
  fprintf fmt "\n"

let print_arrass fmt arrass =
  fprintf fmt "%s" idt;
  let str, strl, term = arrass in
  fprintf fmt "%s[" str;
  print_sep_elmt "," fmt (fun fmt s -> fprintf fmt "%s" s) strl;
  fprintf fmt "] := %a" print_term term

let print_assigns fmt assign =
  fprintf fmt "%s" idt;
  let str, term = assign in
  fprintf fmt "%s := %a\n" str print_term term

let print_uliteral fmt ulit = 
  let ident, satoms = ulit in
  fprintf fmt "forall_other %s . (\n%s%s" ident idt idt;
  print_sep_elmt "\n\t\t|| " fmt (print_satom false) satoms;
  fprintf fmt "\n\t)\n"
    
let print_transition fmt tr =
  fprintf fmt "transition %s (" tr.tr_name;
  print_sep_elmt " " fmt (fun fmt s -> fprintf fmt "%s" s) tr.tr_args; 
  fprintf fmt ")\nrequires {\n";
  print_satom true fmt tr.tr_reqs ;
  if (not (SAtom.is_empty tr.tr_reqs) && (tr.tr_ureq != [])) then 
  fprintf fmt "\n%s&& " idt;
  List.iter (print_uliteral fmt) tr.tr_ureq;
  fprintf fmt "\n}\n";
  fprintf fmt "{\n";
  (*  List.iter (print_action fmt) tr.tr_actions;*)
  print_sep_elmt ";\n" fmt print_assigns tr.tr_assigns;
  if tr.tr_arrass <> [] && tr.tr_assigns <> [] then fprintf fmt ";";
  print_sep_elmt ";\n" fmt print_arrass tr.tr_arrass;
  fprintf fmt "\n";
  (* List.iter (print_arrass fmt) tr.tr_arrass; *)
  List.iter (print_update fmt) tr.tr_upds;
  List.iter (fprintf fmt "%s := .\n") tr.tr_nondets;
  fprintf fmt "}\n\n"

let print_inv fmt (ids, cube) =
  fprintf fmt "invariant (";
  print_sep_elmt " " fmt (fun fmt s -> fprintf fmt "%s" s) ids;
  fprintf fmt ") {\n%a\n}\n" (print_satom true) cube

let print_elem fmt elem =
  let id, constr = elem in 
  fprintf fmt "type %s = " id;
  print_sep_elmt " | " fmt (fun fmt s -> fprintf fmt "%s" s) constr

let print_typedef fmt type_defs =
  print_sep_elmt "\n" fmt print_elem type_defs;
  fprintf fmt "\n"

let print_unsafe fmt (sl, sa) =
  fprintf fmt "unsafe (%a) {\n%a\n}\n\n"
    (fun fmt -> print_sep_elmt " " fmt (fun fmt s -> fprintf fmt "%s" s))
    sl (print_satom true) sa

let print_init fmt (p, sa) = (* optional proc, guard *)
  fprintf fmt "init (%s) {\n%a\n}\n\n"
    (match p with Some s -> s | None -> "") (print_satom true) sa

let print_state fmt = function
| Sinit (so, sa) -> print_init fmt (so, sa)
| Sinv (sl, sa) -> print_inv fmt (sl, sa)
| Scand s -> assert false (* TODO *)
| Sunsafe (sl, sa) -> print_unsafe fmt (sl, sa)
| Sforward (sl1, sl2, sa) -> assert false (* TODO *)
| Strans tr -> print_transition fmt tr

let print_states fmt states = 
  let init, unsafes, trs = ref (None, SAtom.empty), ref [], ref [] in
  let rec split_unsafe_trans states = 
    match states with
    | Slist l -> List.iter (
      fun e ->
        begin match e with
        | Sunsafe _ -> unsafes := e :: !unsafes 
        | Sinit (p, sa) -> init := (p, sa)
        | _ -> trs := e :: !trs end
    ) l
    | Sapp (c1, c2) -> split_unsafe_trans c1; split_unsafe_trans c2
  in
  split_unsafe_trans states;
  print_init fmt !init;
  List.iter (print_state fmt) (List.rev !unsafes);
  List.iter (print_state fmt) (List.rev !trs)
    

let print_decl fmt = function
| Dglobal (v, t) ->
    fprintf fmt "var %s : %s\n" v t
| Dconst (c, t) -> fprintf fmt "const %s : %s\n" c t
| Darray (a, (itl, ct)) -> fprintf fmt "array %s [" a;
    print_sep_elmt "," fmt (fun fmt s -> fprintf fmt "%s" s) itl;
    fprintf fmt "] : %s\n" ct

let rec print_decls fmt = function
| Dlist l -> List.iter (print_decl fmt) l
| Dapp (c1, c2) -> print_decls fmt c1; print_decls fmt c2
  
let print_system fmt system = 
  if system.num_procs > 1 then fprintf fmt "number_procs %d\n" system.num_procs;
  print_typedef fmt system.type_defs;
  fprintf fmt "\n";
  print_decls fmt system.decls;
  fprintf fmt "\n";
  print_states fmt system.states












